Revert "property_checkert interface" #2212
Conversation
tautschnig
requested review from
kroening,
peterschrammel and
smowton
as code owners
|
@kroening @peterschrammel Would you mind providing the high-level idea of how this is supposed to be used? Given the absence of documentation I'll try to reverse-engineer it from 2LS, but receiving brief guidance would be very much appreciated. The main question is: what is this interface supposed to separate, i.e., what is to be moved to the implementation of the interface and what invokes the interface's methods? |
|
The bigger idea is: As a user I want to run one or more property checkers (I can instantiate whatever implementations we have: BMC, path-based symex, incremental BMC, abstract interpretation, k-induction, IC3, ...) and report and fuse results from multiple runs (portfolio, heuristic selection of an appropriate checker or some other strategy). |
|
@peterschrammel : that sounds like a good thing to do / want. Is it worth opening an issue / creating some kind of plan for getting that implemented in the existing CPROVER tools? |
|
@peterschrammel Given all your work, can this now actually be done (i.e., |
|
This still has to wait a bit until symex-driven lazy loading has been ported to goto-checker. |
Symex-driven lazy loading uses goto-checker [blocks: #2212]
Has that time already come now that #4541 is merged? |
|
@peterschrammel ping? |
This reverts commit d88ffd4.
tautschnig
force-pushed
the
property-checker-interface
branch
from
f930065 to
c07449c
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: c07449c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112029630
This reverts commit d88ffd4.
Doing so might not actually be desirable, but the code is neither sufficiently documented nor actually used within the repository (though apparently be 2LS and Deltacheck). Input from @peterschrammel required.